Pull Request Description

Related Issue

This pull request resolves # [add issue number if applicable]

Intended Change

This PR implements the complete desugaring transformation for try-with-resources statements in the KeY Java transformation pipeline. The TryWithResourceReducer class now transforms every try-with-resources statement into the equivalent nested try/finally form that javac generates, enabling KeY to reason about code without requiring native support for try-with-resources syntax.

Technical Details

For a simple try-with-resources:

try (Resource r = open()) {
    body;
}

The transformation produces:

try {
    Resource r = open();
    Throwable primaryExc$1 = null;
    try {
        body;
    } catch (Throwable t$1) {
        primaryExc$1 = t$1;
        throw t$1;
    } finally {
        if (r != null) {
            if (primaryExc$1 != null) {
                try { r.close(); } catch (Throwable suppressedExc$1) {
                    primaryExc$1.addSuppressed(suppressedExc$1);
                }
            } else { 
                r.close(); 
            }
        }
    }
}

Key features:

• Multiple resources are handled by nesting (last-declared resource closes first)
• Any catch/finally clauses attached to the original try are preserved on an outer wrapper
• Supports both Java 8 style try (Resource r = expr) and Java 9+ style try (existingVar) forms
• Properly handles suppressed exceptions per JLS 14.20.3
• Uses unique counter-based variable names to avoid collisions

Type of pull request

• Refactoring (behavior should not change or only minimally change)
• There are changes to the Java code

Ensuring quality

• I made sure that introduced/changed code is well documented (Javadoc and inline comments).
• I added new test case(s) for new functionality.
• I have tested the feature as follows: Test cases

Additional information and contact(s)

Author: @weigl, with contributions from Claude Sonnet

This transformation is part of the broader effort to normalize Java constructs for formal verification in KeY. The implementation follows the exact semantics specified in JLS 14.20.3 and mirrors the bytecode-level transformation performed by javac.

Contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.